L:MsgA List. (L)  MsgAForm 

latex

Definitions	x:A. B(x), t  T, (L), reduce(f;k;as), Y, MsgAForm, , Top, mk-ma, x. t(x), Prop, x(s), MsgA, M1  M2, Valtype(da;k)
Lemmas	msga wf, fpf-empty wf, Id wf, top wf, Knd wf, IdLnk wf, msg-form-join, fpf-trivial-subtype-top, fpf-cap wf, id-deq wf, ma-state wf, Kind-deq wf, locl wf, pi1 wf, pi2 wf, rcv wf